COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00006 00003	.item←0
C00009 00004	.skip 1
C00010 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.turn off "{"
.cb SPECIFICATIONS FOR A NEW FIRST ORDER LOGIC PROOF-CHECKER

	The Stanford Artificial Intelligence Laboratory (SAIL) has
been using a first order logic proof-checker called FOL
for several years and the Institute for Mathematical Studies
in the Social Sciences (IMSSS) at Stanford has been using
a different one.  Both of themm have gotten encrusted with
barnacles and should be replaced which will be a substantial
undertaking.  We both hope that there will be sufficient common
interest so that the work of replacing them can be shared.

	Here are some proposals for specifications:
.item←0
	#. The checker will be interactive, but will also accept
input from files.  These files may require further files.

	#. The new checker will be written in LISP entirely.
Good coding practices will be used.  The program will be
documented for easy modification.  The essential core image
will be kept small, and a MACLISP or equivalent facility
for keeping some functions on disk to be read in when necessary
will be used.

	#. Every expression given an interpretation and every
command will have an internal form as an S-expression.  It will
be possible to make proofs in the internal form, although this
will not be done except for debugging.  Proof generators will
generate proofs in internal form.  The actual commands will
be in a conventional mathematical language that is translated
into internal form by a parser.  The parser must be informative
about errors and should be readily modified.  The machine's
replies will also be in a mathematical form which need not
be identical with input but any expressions printed should be
acceptable also as input.

	#. Operational features will include the ability to
save the state of a proof, to link with editors.

	#. Means will be provided to edit proofs and resubmit
them for checking.  It will be possible to store theorems.

	#. Block structured declarations will be possible.
Typographical declarations will be allowed, e.g. it will be
possible to say that all identifiers beginning with I represent
integer variables.

	#. The internal form of statements will facilitate
metamathematics.
.item←0
	#. Variables and function names will be strings of letters
and digits beginning with letters.  The system itself willl
not have any other typographical conventions.  Such conventions
must be established by declarations.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of

PUBbed at {time} on {date}.%1